Example 9 in [Borralleras, Lucas & Rubio - CADE'02]

Summary: Ex9_BLR02

• CS-TRS format
• OBJ format
• Negative results:
• Positive results:
  1. Lucas' transformation (Polynomials @ MuTerm)
  2. Zantema's transformation (DP+Poly @ CiME)
  3. Ferreira and Ribeiro's transformation (Corollary)
  4. Giesl and Middeldorp's transformation (DP+Poly @ CiME)
  5. CSRPO
  6. Polynomial interpretation (MuTerm)
  7. CSDP

CS-TRS Ex9_BLR02 (file Ex9_BLR02.csr)

Functions:  filter cons 0 s sieve nats zprimes

Constructors:  cons 0 s

Variables:  X Y M N

Arities: 

ar(filter) = 3
ar(cons) = 2
ar(0) = 0
ar(s) = 1
ar(sieve) = 1
ar(nats) = 1
ar(zprimes) = 0

Replacement map: 

µ(filter)={1,2,3}
µ(cons)={1}
µ(0)={}
µ(s)={1}
µ(sieve)={1}
µ(nats)={1}
µ(zprimes)={1}

Rules:  (file Ex9_BLR02)   

filter(cons(X,Y),0,M) -> cons(0,filter(Y,M,M))
filter(cons(X,Y),s(N),M) -> cons(X,filter(Y,N,M))
sieve(cons(0,Y)) -> cons(0,sieve(Y))
sieve(cons(s(N),Y)) -> cons(s(N),sieve(filter(Y,N,N)))
nats(N) -> cons(N,nats(s(N)))
zprimes -> sieve(nats(s(s(0))))

The CS-TRS in OBJ format (file Ex9_BLR02.obj):

obj Ex9_BLR02 is
  sort S .
  op filter : S S S -> S .
  op cons : S S -> S [strat (1 0)] .
  op 0 : -> S .
  op s : S -> S .
  op sieve : S -> S .
  op nats : S -> S .
  op zprimes : -> S .
  vars X Y M N : S .
  eq filter(cons(X,Y),0,M) = cons(0,filter(Y,M,M)) .
  eq filter(cons(X,Y),s(N),M) = cons(X,filter(Y,N,M)) .
  eq sieve(cons(0,Y)) = cons(0,sieve(Y)) .
  eq sieve(cons(s(N),Y)) = cons(s(N),sieve(filter(Y,N,N))) .
  eq nats(N) = cons(N,nats(s(N))) .
  eq zprimes = sieve(nats(s(s(0)))) .
endo

Negative results

Positive results

1. Ex9_BLR02 can be proved µ-terminating by using Lucas' transformation. The TRS Ex9_BLR02_L:

       filter(cons(X),0,M) -> cons(0)
       filter(cons(X),s(N),M) -> cons(X)
       sieve(cons(0)) -> cons(0)
       sieve(cons(s(N))) -> cons(s(N))
       nats(N) -> cons(N)
       zprimes -> sieve(nats(s(s(0))))
       

   can be proved terminating by using a polynomial interpretation (use MuTerm)
2. Ex9_BLR02 can be proved µ-terminating by using Zantema's transformation. The TRS Ex9_BLR02_Z:

       filter(cons(X,Y),0,M) -> cons(0,n__filter(activate(Y),M,M))
       filter(cons(X,Y),s(N),M) -> cons(X,n__filter(activate(Y),N,M))
       sieve(cons(0,Y)) -> cons(0,n__sieve(activate(Y)))
       sieve(cons(s(N),Y)) -> cons(s(N),n__sieve(filter(activate(Y),N,N)))
       nats(N) -> cons(N,n__nats(s(N)))
       zprimes -> sieve(nats(s(s(0))))
       filter(X1,X2,X3) -> n__filter(X1,X2,X3)
       sieve(X) -> n__sieve(X)
       nats(X) -> n__nats(X)
       activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3)
       activate(n__sieve(X)) -> sieve(X)
       activate(n__nats(X)) -> nats(X)
       activate(X) -> X
       

   can be proved terminating (use dependency pairs approach with CiME).
3. By [GM04, Theorem 11], the µ-termination of Ex9_BLR02 can also be proved by using Ferreira and Ribeiro's transformation (but no concrete proof has been reported yet).
4. The µ-termination of Ex9_BLR02 can also be proved by using Giesl and Middeldorp's transformation: the TRS Ex9_BLR02_GM:

       a__filter(cons(X,Y),0,M) -> cons(0,filter(Y,M,M))
       a__filter(cons(X,Y),s(N),M) -> cons(mark(X),filter(Y,N,M))
       a__sieve(cons(0,Y)) -> cons(0,sieve(Y))
       a__sieve(cons(s(N),Y)) -> cons(s(mark(N)),sieve(filter(Y,N,N)))
       a__nats(N) -> cons(mark(N),nats(s(N)))
       a__zprimes -> a__sieve(a__nats(s(s(0))))
       mark(filter(X1,X2,X3)) -> a__filter(mark(X1),mark(X2),mark(X3))
       mark(sieve(X)) -> a__sieve(mark(X))
       mark(nats(X)) -> a__nats(mark(X))
       mark(zprimes) -> a__zprimes
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       mark(0) -> 0
       mark(s(X)) -> s(mark(X))
       a__filter(X1,X2,X3) -> filter(X1,X2,X3)
       a__sieve(X) -> sieve(X)
       a__nats(X) -> nats(X)
       a__zprimes -> zprimes
       

   can be proved terminating (use the dependency pairs approach with CiME).
5. The µ-termination of Ex9_BLR02 is proved in [BLR02, Example 9] by using CSRPO and automatically by MuTerm.
   • marking map:

     	   m(cons,2)=m(_cons,2)=m(_filter,1)=m(_sieve,1)={filter,sieve,nats}
     	   

   • precedence:

     	   zprimes > sieve, nats, s, 0
     	   nats > cons, _nats, s
     	   sieve > cons, _sieve, _filter
     	   filter > cons, _filter
     	   

   • status:

     	   st(f)=mul for all symbols f.
     	   

6. The µ-termination of Ex9_BLR02 can also be proved by using a polynomial interpretation computed with MuTerm:

       [filter](X1,X2,X3) = 2.X1 + X2 + X3
       [cons](X1,X2) = X1 + 1
       [0] = 0
       [s](X) = X
       [sieve](X) = 2.X
       [nats](X) = X + 2
       [zprimes] = 5
       

7. The µ-termination of Ex9_BLR02 can also be proved by using CSDP computed by MuTerm.